\begin{tabbing}
(\=RA ((Assert ({-}($i$+$j$)) $\leq$ ({-}($i$+$j$))) \+
\\[0ex]CollapseTHENM (
\-\\[0ex]FwdThruLemma `add\_functionality\_wrt\_le` [3;{-}1]))$\cdot$)
\end{tabbing}